{-# LANGUAGE NoImplicitPrelude #-}

-- Copyright (C) 2016 Koz Ross <koz.ross@retro-freedom.nz>

-- This program is free software: you can redistribute it and/or modify
-- it under the terms of the GNU General Public License as published by
-- the Free Software Foundation, either version 3 of the License, or
-- (at your option) any later version.

-- This program is distributed in the hope that it will be useful,
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-- GNU General Public License for more details.

-- You should have received a copy of the GNU General Public License
-- along with this program.  If not, see <http://www.gnu.org/licenses/>.

module Test (tests) where

import BasicPrelude hiding (empty)

import Distribution.TestSuite

import Test.QuickCheck

import Data.Logic.DNF

tests :: IO [Test]
tests = return . fmap Test $ [testInterpreter, testOptimizer, testNegator]

testInterpreter :: TestInstance
testInterpreter = TestInstance {
  run = do
      res <- quickCheckWithResult stdArgs {maxSuccess = 500, maxSize = 10} prop_correct
      case res of
        Success {} -> return . Finished $ Pass
        _ -> return . Finished $ Fail "Failed interpreter correctness checks",
  name = "Interpreter correctness check",
  tags = [],
  options = [],
  setOption = \_ _ -> Right testInterpreter}
  where prop_correct :: Interpretation -> Form -> Bool
        prop_correct interp f = let res = interpret interp f
                                    canonical = interpretSafe interp f in
          case res of
            Just _ -> res == canonical
            Nothing -> True

testNegator :: TestInstance
testNegator = TestInstance {
  run = do
      res <- quickCheckWithResult stdArgs {maxSuccess = 500, maxSize = 4} prop_negate
      case res of
        Success {} -> return . Finished $ Pass
        _ -> return . Finished $ Fail "Failed negator correctness checks",
  name = "Negation behaviour check",
  tags = [],
  options = [],
  setOption = \_ _ -> Right testOptimizer}
  where prop_negate :: Interpretation -> Form -> Bool
        prop_negate interp f = let f' = invert f in
          case interpret interp f of
            Just x -> interpret interp f' /= Just x
            Nothing -> True


testOptimizer :: TestInstance
testOptimizer = TestInstance {
  run = do
      res <- quickCheckWithResult stdArgs {maxSuccess = 500, maxSize = 10} prop_equivalent
      case res of
        Success {} -> return . Finished $ Pass
        _ -> return . Finished $ Fail "Failed optimizer correctness checks",
  name = "Optimizer behaviour check",
  tags = [],
  options = [],
  setOption = \_ _ -> Right testOptimizer}
  where prop_equivalent :: Interpretation -> Form -> Bool
        prop_equivalent interp f = case interpret interp f of
          Nothing -> True
          Just x -> join (interpret interp <$> optimize f) /= Just (not x)
